Formal verification is now an industrial strength solution that is used on small designs, or design components, to identify bugs. Model checkers are used to check if desired properties hold on a design. Equivalence checkers are used to show that two designs, usually at different abstraction levels (e.g. verilog vs. netlist), are equivalent.
Equivalence checkers can verify equivalence between RTL (Register Transfer Level) descriptions, RTL design and gate-level design, between gate-level designs, and between gate-to-transistor comparisons. They employ formal mathematical techniques to prove that two versions of a design are functionally equivalent.
A model checker reviews a single model. Given the model and a set of desired properties, the model checker explores the full state space of the model to check whether the given properties are satisfied by the model. The model checker either verifies the given properties or generates counter examples. There are cases in which the model checker, due to the size of the problem, cannot provide any conclusive answers to the problem.
The main barrier for the general acceptance of these and other formal verification tools is that they require highly skilled users. For example, model checkers require that assertions be written and that they be written in temporal logic. Towards enabling the use of the tools by less sophisticated users, the idea of implied intent was raised. Generally speaking, systems for implied intent attempt to look at the code, figure out what the user meant for the code or the design to implement, and check, using the formal tools, if it is implemented.
The concept of “Coverability”, as described by Gil Ratsaby, Baruch Sterin and Shmuel Ur in “Improvements in Coverability Analysis”. FME 2002: 41-56, checks, for example, that every statement in a program is reachable.
It will be appreciated that for simplicity and clarity of illustration, elements shown in the figures have not necessarily been drawn to scale. For example, the dimensions of some of the elements may be exaggerated relative to other elements for clarity. Further, where considered appropriate, reference numerals can be repeated among the figures to indicate corresponding or analogous elements.